Nuprl Lemma : pairs-fpf_wf
11,40
postcript
pdf
A
,
B
:Type,
eq1
:EqDecider(
A
),
eq2
:EqDecider(
B
),
L
:((
:
A
B
) List). fpf(
L
)
a
:
A
fp
B
List
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
EqDecider(
T
)
,
(
x
l
)
,
x
.
t
(
x
)
,
t
.1
,
map(
f
;
as
)
,
remove-repeats(
eq
;
L
)
,
t
.2
,
insert(
a
;
L
)
,
eqof(
d
)
,
if
b
then
t
else
f
fi
,
reduce(
f
;
k
;
as
)
,
fpf(
L
)
,
a
:
A
fp
B
(
a
)
Lemmas
reduce
wf
,
ifthenelse
wf
,
eqof
wf
,
insert
wf
,
pi2
wf
,
remove-repeats
wf
,
map
wf
,
pi1
wf
,
l
member
wf
,
deq
wf
origin
A, B:Type, eq1:EqDecider(A), eq2:EqDecider(B), L:((:A 
B) List). fpf(L) 
a:A fp
B List A, B:Type, eq1:EqDecider(A), eq2:EqDecider(B), L:((:A B) List). fpf(L) a:A fp B List Tx:A. B(x) l)
x. t(x) B(a)